Bob is furry. Charlie is nice. Charlie is round. Fiona is not red. Fiona is not white. Gary is furry. Gary is round. If someone is furry then they are young. All young people are red. If someone is red then they are big. Round, big people are furry. If Fiona is big and Fiona is not white then Fiona is not nice. If Charlie is big then Charlie is furry. If someone is white and not young then they are nice. All young people are nice.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Round, big people are furry.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Fiona is big and Fiona is not white then Fiona is not nice.
((("Fiona" "is" "big" "+") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "nice" "-"))
If Charlie is big then Charlie is furry.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is white and not young then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Gary is round.
True
1
proof
[(triple7)]
("Gary" "is" "round" "+")
triple7
Fiona is red.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "red" "+")
triple4
Gary is young.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "young" "+")
((triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "-")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule8))]
("Gary" "is" "nice" "-")
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
True
4
proof
[(((((((triple6) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not big.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "big" "-")
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Fiona is nice.
Unknown
rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@5: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is furry.[(triple1)] Charlie is nice.[(triple2)] Charlie is round.[(triple3)] Fiona is not red.[(triple4)] Fiona is not white.[(triple5)] Gary is furry.[(triple6)] Gary is round.[(triple7)] @1: Bob is young.[(((triple1) -> rule1))] Gary is young.[(((triple6) -> rule1))] @2: Bob is nice.[(((((triple1) -> rule1)) -> rule8))] Bob is red.[(((((triple1) -> rule1)) -> rule2))] Gary is nice.[(((((triple6) -> rule1)) -> rule8))] Gary is red.[(((((triple6) -> rule1)) -> rule2))] @3: Bob is big.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))] Gary is big.[(((((((triple6) -> rule1)) -> rule2)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Fiona is not red.
("Fiona" "is" "red" "-")
triple4
Fiona is not white.
("Fiona" "is" "white" "-")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3