Bob is big. Bob is round. Charlie is big. Erin is blue. Harry is blue. Harry is round. Harry is young. All young things are cold. All big, blue things are young. If something is smart then it is big. If something is big then it is kind. If something is cold and blue then it is round. If something is round and kind then it is blue. All cold things are young. All cold things are young. If Erin is blue then Erin is smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All big, blue things are young.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is cold and blue then it is round.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is round and kind then it is blue.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Erin is blue then Erin is smart.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "smart" "+"))
Harry is round.
True
1
proof
[(triple6 OR ((((triple7) -> rule1) triple5) -> rule5))]
("Harry" "is" "round" "+")
triple6
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is big.
True
3
proof
[(((((triple4) -> rule9)) -> rule3))]
("Erin" "is" "big" "+")
((((triple4) -> (rule9 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple2 ((triple1) -> rule4)) -> rule6))]
("Bob" "is" "blue" "-")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
True
6
proof
[(((triple1 ((triple2 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("Bob" "is" "young" "+")
((triple1 ((triple2 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not young.
False
6
inv-proof
[(((triple1 ((triple2 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("Bob" "is" "young" "-")
((triple1 ((triple2 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is cold.
True
6
proof
[(((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1))]
("Erin" "is" "cold" "+")
((((((((triple4) -> (rule9 % int4))) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not cold.
False
6
inv-proof
[(((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1))]
("Erin" "is" "cold" "-")
((((((((triple4) -> (rule9 % int4))) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is round.
True
8
proof
[(((((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1) triple4) -> rule5))]
("Erin" "is" "round" "+")
((((((((((triple4) -> (rule9 % int5))) -> (rule3 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Erin is not round.
False
8
inv-proof
[(((((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1) triple4) -> rule5))]
("Erin" "is" "round" "-")
((((((((((triple4) -> (rule9 % int5))) -> (rule3 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is young.
Unknown
rconc
[@5: Charlie is young.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule2 <- rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is cold.
Unknown
rconc
[@4: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is big.[(triple1)] Bob is round.[(triple2)] Charlie is big.[(triple3)] Erin is blue.[(triple4)] Harry is blue.[(triple5)] Harry is round.[(triple6 OR ((((triple7) -> rule1) triple5) -> rule5))] Harry is young.[(triple7)] @1: Bob is kind.[(((triple1) -> rule4))] Charlie is kind.[(((triple3) -> rule4))] Erin is smart.[(((triple4) -> rule9))] Harry is cold.[(((triple7) -> rule1))] @2: Bob is blue.[(((triple2 ((triple1) -> rule4)) -> rule6))] Erin is big.[(((((triple4) -> rule9)) -> rule3))] @3: Bob is young.[(((triple1 ((triple2 ((triple1) -> rule4)) -> rule6)) -> rule2))] Erin is kind.[(((((((triple4) -> rule9)) -> rule3)) -> rule4))] Erin is young.[(((((((triple4) -> rule9)) -> rule3) triple4) -> rule2))] @4: Bob is cold.[(((((triple1 ((triple2 ((triple1) -> rule4)) -> rule6)) -> rule2)) -> rule1))] Erin is cold.[(((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1))] @5: Erin is round.[(((((((((((triple4) -> rule9)) -> rule3) triple4) -> rule2)) -> rule1) triple4) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple4) -> (rule9 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple1 ((triple2 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple4) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((((triple4) -> (rule9 % int3))) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1 ((triple2 ((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
((((((((triple4) -> (rule9 % int4))) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((((((((((triple4) -> (rule9 % int5))) -> (rule3 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5