Bob is rough. Bob is white. Charlie is blue. Charlie is cold. Charlie is quiet. Erin is nice. Erin is rough. Erin is young. Gary is nice. Gary is young. If Bob is blue then Bob is cold. Nice, young things are quiet. Nice things are cold. If something is nice then it is blue. Quiet, rough things are nice. All nice, quiet things are blue. All quiet, white things are rough. If something is quiet and cold then it is white.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
If Bob is blue then Bob is cold.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "+"))
Nice, young things are quiet.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Quiet, rough things are nice.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All nice, quiet things are blue.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All quiet, white things are rough.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and cold then it is white.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Erin is rough.
True
1
proof
[(triple7 OR ((((triple6 triple8) -> rule2) ((((triple6 triple8) -> rule2) ((triple6) -> rule3)) -> rule8)) -> rule7))]
("Erin" "is" "rough" "+")
triple7
((((triple6 triple8) -> (rule2 % int4)) ((((triple6 triple8) -> (rule2 % int4)) ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is not nice.
False
1
inv-proof
[(triple6)]
("Erin" "is" "nice" "-")
triple6
Erin is cold.
True
2
proof
[(((triple6) -> rule3))]
("Erin" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Charlie is not white.
False
3
inv-proof
[(((triple5 triple4) -> rule8))]
("Charlie" "is" "white" "-")
((triple5 triple4) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
True
5
proof
[(((triple5 ((triple5 triple4) -> rule8)) -> rule7))]
("Charlie" "is" "rough" "+")
((triple5 ((triple5 triple4) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
False
5
inv-proof
[(((triple5 ((triple5 triple4) -> rule8)) -> rule7))]
("Charlie" "is" "rough" "-")
((triple5 ((triple5 triple4) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is rough.
True
10
proof
[(((((triple9 triple10) -> rule2) ((((triple9 triple10) -> rule2) ((triple9) -> rule3)) -> rule8)) -> rule7))]
("Gary" "is" "rough" "+")
((((triple9 triple10) -> (rule2 % int4)) ((((triple9 triple10) -> (rule2 % int4)) ((triple9) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not rough.
False
10
inv-proof
[(((((triple9 triple10) -> rule2) ((((triple9 triple10) -> rule2) ((triple9) -> rule3)) -> rule8)) -> rule7))]
("Gary" "is" "rough" "-")
((((triple9 triple10) -> (rule2 % int4)) ((((triple9 triple10) -> (rule2 % int4)) ((triple9) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is rough.[(triple1)] Bob is white.[(triple2)] Charlie is blue.[(triple3 OR ((((triple5 ((triple5 ((triple5 triple4) -> rule8)) -> rule7)) -> rule5)) -> rule4) OR ((((triple5 ((triple5 ((triple5 triple4) -> rule8)) -> rule7)) -> rule5) triple5) -> rule6))] Charlie is cold.[(triple4)] Charlie is quiet.[(triple5)] Erin is nice.[(triple6)] Erin is rough.[(triple7 OR ((((triple6 triple8) -> rule2) ((((triple6 triple8) -> rule2) ((triple6) -> rule3)) -> rule8)) -> rule7))] Erin is young.[(triple8)] Gary is nice.[(triple9)] Gary is young.[(triple10)] @1: Charlie is white.[(((triple5 triple4) -> rule8))] Erin is blue.[(((triple6) -> rule4) OR ((triple6 ((triple6 triple8) -> rule2)) -> rule6))] Erin is cold.[(((triple6) -> rule3))] Erin is quiet.[(((triple6 triple8) -> rule2))] Gary is blue.[(((triple9) -> rule4) OR ((triple9 ((triple9 triple10) -> rule2)) -> rule6))] Gary is cold.[(((triple9) -> rule3))] Gary is quiet.[(((triple9 triple10) -> rule2))] @2: Charlie is rough.[(((triple5 ((triple5 triple4) -> rule8)) -> rule7))] Erin is white.[(((((triple6 triple8) -> rule2) ((triple6) -> rule3)) -> rule8))] Gary is white.[(((((triple9 triple10) -> rule2) ((triple9) -> rule3)) -> rule8))] @3: Charlie is nice.[(((triple5 ((triple5 ((triple5 triple4) -> rule8)) -> rule7)) -> rule5))] Gary is rough.[(((((triple9 triple10) -> rule2) ((((triple9 triple10) -> rule2) ((triple9) -> rule3)) -> rule8)) -> rule7))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
((((triple5 ((triple5 ((triple5 triple4) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((triple5 ((triple5 ((triple5 triple4) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((((triple6 triple8) -> (rule2 % int4)) ((((triple6 triple8) -> (rule2 % int4)) ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Charlie is white.
("Charlie" "is" "white" "+")
((triple5 triple4) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple6 ((triple6 triple8) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple6 triple8) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple9) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple9 ((triple9 triple10) -> (rule2 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple9 triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5 ((triple5 triple4) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple6 triple8) -> (rule2 % int3)) ((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((triple9 triple10) -> (rule2 % int3)) ((triple9) -> (rule3 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple5 ((triple5 ((triple5 triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((triple9 triple10) -> (rule2 % int4)) ((((triple9 triple10) -> (rule2 % int4)) ((triple9) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4