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