Charlie is big. Charlie is furry. Erin is big. Erin is kind. Erin is smart. Fiona is big. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is smart. Fiona is young. Gary is cold. Gary is furry. Gary is smart. Gary is young. Nice, kind things are cold. Young things are cold. All big things are kind. Smart things are young. All furry things are big. If something is big and cold then it is nice. If something is nice and big then it is young. Young, smart things are cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Nice, kind things are cold.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big and cold then it is nice.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice and big then it is young.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Young, smart things are cold.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Gary is young.
True
1
proof
[(triple15 OR ((triple14) -> rule4) OR ((((((triple13) -> rule5) triple12) -> rule6) ((triple13) -> rule5)) -> rule7))]
("Gary" "is" "young" "+")
triple15
((triple14) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((((triple13) -> (rule5 % int3)) triple12) -> (rule6 % int2)) ((triple13) -> (rule5 % int3))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5))]
("Charlie" "is" "big" "-")
triple1
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
True
2
proof
[(((triple1) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is nice.
True
4
proof
[(((((triple13) -> rule5) triple12) -> rule6) OR ((((triple13) -> rule5) ((triple15) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((triple15 triple14) -> rule8)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4)) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4) triple14) -> rule8)) -> rule6))]
("Gary" "is" "nice" "+")
((((triple13) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple13) -> (rule5 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int3)) ((triple15 triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3)) triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is not nice.
False
4
inv-proof
[(((((triple13) -> rule5) triple12) -> rule6) OR ((((triple13) -> rule5) ((triple15) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((triple15 triple14) -> rule8)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4)) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4) triple14) -> rule8)) -> rule6))]
("Gary" "is" "nice" "-")
((((triple13) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple13) -> (rule5 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int3)) ((triple15 triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3)) triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Erin is nice.
True
5
proof
[(((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule6) OR ((triple3 ((((triple5) -> rule4) triple5) -> rule8)) -> rule6))]
("Erin" "is" "nice" "+")
((triple3 ((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple3 ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule6) OR ((triple3 ((((triple5) -> rule4) triple5) -> rule8)) -> rule6))]
("Erin" "is" "nice" "-")
((triple3 ((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple3 ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is cold.
Unknown
rconc
[@4: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule5))] Charlie is furry.[(triple2)] Erin is big.[(triple3)] Erin is kind.[(triple4 OR ((triple3) -> rule3))] Erin is smart.[(triple5)] Fiona is big.[(triple6)] Fiona is cold.[(triple7 OR ((triple11) -> rule2) OR ((triple11 triple10) -> rule8) OR ((triple9 triple8) -> rule1) OR ((((triple10) -> rule4)) -> rule2) OR ((((triple9 triple6) -> rule7)) -> rule2) OR ((triple9 ((triple6) -> rule3)) -> rule1) OR ((((triple10) -> rule4) triple10) -> rule8) OR ((((triple9 triple6) -> rule7) triple10) -> rule8))] Fiona is kind.[(triple8 OR ((triple6) -> rule3))] Fiona is nice.[(triple9 OR ((triple6 triple7) -> rule6) OR ((triple6 ((triple11) -> rule2)) -> rule6) OR ((triple6 ((triple11 triple10) -> rule8)) -> rule6) OR ((triple6 ((((triple10) -> rule4)) -> rule2)) -> rule6) OR ((triple6 ((((triple10) -> rule4) triple10) -> rule8)) -> rule6))] Fiona is smart.[(triple10)] Fiona is young.[(triple11 OR ((triple10) -> rule4) OR ((triple9 triple6) -> rule7) OR ((((triple6 triple7) -> rule6) triple6) -> rule7))] Gary is cold.[(triple12 OR ((triple15) -> rule2) OR ((triple15 triple14) -> rule8) OR ((((triple14) -> rule4)) -> rule2) OR ((((triple14) -> rule4) triple14) -> rule8))] Gary is furry.[(triple13)] Gary is smart.[(triple14)] Gary is young.[(triple15 OR ((triple14) -> rule4) OR ((((((triple13) -> rule5) triple12) -> rule6) ((triple13) -> rule5)) -> rule7))] @1: Charlie is kind.[(((triple1) -> rule3) OR ((((triple2) -> rule5)) -> rule3))] Erin is young.[(((triple5) -> rule4))] Gary is big.[(((triple13) -> rule5))] @2: Erin is cold.[(((((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple5) -> rule8))] Gary is kind.[(((((triple13) -> rule5)) -> rule3))] Gary is nice.[(((((triple13) -> rule5) triple12) -> rule6) OR ((((triple13) -> rule5) ((triple15) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((triple15 triple14) -> rule8)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4)) -> rule2)) -> rule6) OR ((((triple13) -> rule5) ((((triple14) -> rule4) triple14) -> rule8)) -> rule6))] @3: Erin is nice.[(((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule6) OR ((triple3 ((((triple5) -> rule4) triple5) -> rule8)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple3) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
((triple11) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple11 triple10) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple9 triple8) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 triple6) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((triple9 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple10) -> (rule4 % int2)) triple10) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 triple6) -> (rule7 % int2)) triple10) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
((triple6) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple6 triple7) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple6 ((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((triple11 triple10) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((triple6 ((((triple10) -> (rule4 % int3)) triple10) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple10) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9 triple6) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple6 triple7) -> (rule6 % int2)) triple6) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple15) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple15 triple14) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple14) -> (rule4 % int2)) triple14) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
((triple14) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((((triple13) -> (rule5 % int3)) triple12) -> (rule6 % int2)) ((triple13) -> (rule5 % int3))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple13) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple13) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple13) -> (rule5 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int3)) ((triple15 triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple13) -> (rule5 % int4)) ((((triple14) -> (rule4 % int3)) triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((triple3 ((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple3 ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3