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