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