Dave is cold. Erin is cold. Erin is green. Erin is quiet. Erin is red. Erin is young. Harry is smart. All big, smart things are young. If Erin is cold then Erin is red. If something is smart then it is big. If something is big and young then it is green. Smart, red things are young. Green things are cold. If Erin is big and Erin is cold then Erin is young. If something is young and green then it is cold.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All big, smart things are young.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Erin is cold then Erin is red.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "red" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is big and young then it is green.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Smart, red things are young.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Erin is big and Erin is cold then Erin is young.
((("Erin" "is" "big" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "young" "+"))
If something is young and green then it is cold.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Erin is green.
True
1
proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Erin is not quiet.
False
1
inv-proof
[(triple4)]
("Erin" "is" "quiet" "-")
triple4
Harry is big.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "big" "+")
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "big" "-")
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
True
4
proof
[(((((triple7) -> rule3) triple7) -> rule1))]
("Harry" "is" "young" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not young.
False
4
inv-proof
[(((((triple7) -> rule3) triple7) -> rule1))]
("Harry" "is" "young" "-")
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
True
7
proof
[(((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule1)) -> rule4))]
("Harry" "is" "green" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not green.
False
7
inv-proof
[(((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule1)) -> rule4))]
("Harry" "is" "green" "-")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is cold.[(triple1)] Erin is cold.[(triple2 OR ((triple3) -> rule6) OR ((triple6 triple3) -> rule8))] Erin is green.[(triple3)] Erin is quiet.[(triple4)] Erin is red.[(triple5 OR ((triple2) -> rule2) OR ((((triple3) -> rule6)) -> rule2) OR ((((triple6 triple3) -> rule8)) -> rule2))] Erin is young.[(triple6)] Harry is smart.[(triple7)] @1: Harry is big.[(((triple7) -> rule3))] @2: Harry is young.[(((((triple7) -> rule3) triple7) -> rule1))] @3: Harry is green.[(((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule1)) -> rule4))] @4: Harry is cold.[(((((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule1)) -> rule4)) -> rule6) OR ((((((triple7) -> rule3) triple7) -> rule1) ((((triple7) -> rule3) ((((triple7) -> rule3) triple7) -> rule1)) -> rule4)) -> rule8))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple6 triple3) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple6 triple3) -> (rule8 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7) -> (rule3 % int4)) ((((triple7) -> (rule3 % int4)) triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((((triple7) -> (rule3 % int4)) triple7) -> (rule1 % int3)) ((((triple7) -> (rule3 % int4)) ((((triple7) -> (rule3 % int4)) triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4