Anne is cold. Anne is kind. Bob is cold. Bob is rough. Bob is white. Dave is rough. Fiona is cold. Fiona is rough. Fiona is smart. Fiona is white. If Anne is young then Anne is round. Round, kind people are smart. Kind people are young. All white, rough people are young. If someone is cold and young then they are round. All white, cold people are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Anne is young then Anne is round.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "round" "+"))
Round, kind people are smart.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All white, rough people are young.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and young then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All white, cold people are smart.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Fiona is white.
True
1
proof
[(triple10)]
("Fiona" "is" "white" "+")
triple10
Fiona is not smart.
False
1
inv-proof
[(triple9 OR ((triple10 triple7) -> rule6))]
("Fiona" "is" "smart" "-")
triple9
((triple10 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
True
3
proof
[(((triple10 triple8) -> rule4))]
("Fiona" "is" "young" "+")
((triple10 triple8) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is not young.
False
3
inv-proof
[(((triple5 triple4) -> rule4))]
("Bob" "is" "young" "-")
((triple5 triple4) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is round.
True
5
proof
[(((triple7 ((triple10 triple8) -> rule4)) -> rule5))]
("Fiona" "is" "round" "+")
((triple7 ((triple10 triple8) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1) OR ((triple1 ((triple2) -> rule3)) -> rule5))]
("Anne" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple1 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple2) -> rule3)) -> rule1) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule3)) -> rule5) triple2) -> rule2))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((((triple2) -> rule3)) -> rule1) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule3)) -> rule5) triple2) -> rule2))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Bob is cold.[(triple3)] Bob is rough.[(triple4)] Bob is white.[(triple5)] Dave is rough.[(triple6)] Fiona is cold.[(triple7)] Fiona is rough.[(triple8)] Fiona is smart.[(triple9 OR ((triple10 triple7) -> rule6))] Fiona is white.[(triple10)] @1: Anne is young.[(((triple2) -> rule3))] Bob is smart.[(((triple5 triple3) -> rule6))] Bob is young.[(((triple5 triple4) -> rule4))] Fiona is young.[(((triple10 triple8) -> rule4))] @2: Anne is round.[(((((triple2) -> rule3)) -> rule1) OR ((triple1 ((triple2) -> rule3)) -> rule5))] Bob is round.[(((triple3 ((triple5 triple4) -> rule4)) -> rule5))] Fiona is round.[(((triple7 ((triple10 triple8) -> rule4)) -> rule5))] @3: Anne is smart.[(((((((triple2) -> rule3)) -> rule1) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule3)) -> rule5) triple2) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
((triple10 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple5 triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple5 triple4) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple10 triple8) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple1 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple3 ((triple5 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple7 ((triple10 triple8) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3