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