Bob is big. Bob is green. Bob is quiet. Bob is young. Charlie is big. Charlie is green. Charlie is quiet. Charlie is rough. Erin is big. Erin is green. Erin is quiet. Erin is young. Harry is cold. Harry is green. Harry is rough. Harry is young. Kind things are young. All rough things are green. If Harry is quiet and Harry is young then Harry is rough. If something is kind and quiet then it is rough. All cold, young things are kind. If Bob is rough and Bob is big then Bob is kind. All cold, green things are big. All young, green things are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If Harry is quiet and Harry is young then Harry is rough.
((("Harry" "is" "quiet" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "rough" "+"))
If something is kind and quiet then it is rough.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All cold, young things are kind.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If Bob is rough and Bob is big then Bob is kind.
((("Bob" "is" "rough" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "kind" "+"))
All cold, green things are big.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All young, green things are cold.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Bob is quiet.
True
1
proof
[(triple3)]
("Bob" "is" "quiet" "+")
triple3
Bob is not big.
False
1
inv-proof
[(triple1 OR ((((triple4 triple2) -> rule8) triple2) -> rule7))]
("Bob" "is" "big" "-")
triple1
((((triple4 triple2) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Harry is big.
True
3
proof
[(((triple13 triple14) -> rule7) OR ((triple13 ((triple15) -> rule2)) -> rule7) OR ((((triple16 triple14) -> rule8) triple14) -> rule7) OR ((((triple16 triple14) -> rule8) ((triple15) -> rule2)) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) triple14) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) ((triple15) -> rule2)) -> rule7))]
("Harry" "is" "big" "+")
((triple13 triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple16 triple14) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16 triple14) -> (rule8 % int3)) ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) ((triple15) -> (rule2 % int3))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not big.
False
3
inv-proof
[(((triple13 triple14) -> rule7) OR ((triple13 ((triple15) -> rule2)) -> rule7) OR ((((triple16 triple14) -> rule8) triple14) -> rule7) OR ((((triple16 triple14) -> rule8) ((triple15) -> rule2)) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) triple14) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) ((triple15) -> rule2)) -> rule7))]
("Harry" "is" "big" "-")
((triple13 triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple16 triple14) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16 triple14) -> (rule8 % int3)) ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) ((triple15) -> (rule2 % int3))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is kind.
True
5
proof
[(((((triple4 triple2) -> rule8) triple4) -> rule5))]
("Bob" "is" "kind" "+")
((((triple4 triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
False
5
inv-proof
[(((((triple4 triple2) -> rule8) triple4) -> rule5))]
("Bob" "is" "kind" "-")
((((triple4 triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
True
7
proof
[(((((((triple4 triple2) -> rule8) triple4) -> rule5) triple3) -> rule4))]
("Bob" "is" "rough" "+")
((((((triple4 triple2) -> (rule8 % int3)) triple4) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Erin is not rough.
False
7
inv-proof
[(((((((triple12 triple10) -> rule8) triple12) -> rule5) triple11) -> rule4))]
("Erin" "is" "rough" "-")
((((((triple12 triple10) -> (rule8 % int3)) triple12) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not cold.
Unknown
inv-rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is big.[(triple1 OR ((((triple4 triple2) -> rule8) triple2) -> rule7))] Bob is green.[(triple2)] Bob is quiet.[(triple3)] Bob is young.[(triple4)] Charlie is big.[(triple5)] Charlie is green.[(triple6 OR ((triple8) -> rule2))] Charlie is quiet.[(triple7)] Charlie is rough.[(triple8)] Erin is big.[(triple9 OR ((((triple12 triple10) -> rule8) triple10) -> rule7))] Erin is green.[(triple10)] Erin is quiet.[(triple11)] Erin is young.[(triple12)] Harry is cold.[(triple13 OR ((triple16 triple14) -> rule8) OR ((triple16 ((triple15) -> rule2)) -> rule8))] Harry is green.[(triple14 OR ((triple15) -> rule2))] Harry is rough.[(triple15)] Harry is young.[(triple16)] @1: Bob is cold.[(((triple4 triple2) -> rule8))] Erin is cold.[(((triple12 triple10) -> rule8))] Harry is big.[(((triple13 triple14) -> rule7) OR ((triple13 ((triple15) -> rule2)) -> rule7) OR ((((triple16 triple14) -> rule8) triple14) -> rule7) OR ((((triple16 triple14) -> rule8) ((triple15) -> rule2)) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) triple14) -> rule7) OR ((((triple16 ((triple15) -> rule2)) -> rule8) ((triple15) -> rule2)) -> rule7))] Harry is kind.[(((triple13 triple16) -> rule5) OR ((((triple16 triple14) -> rule8) triple16) -> rule5) OR ((((triple16 ((triple15) -> rule2)) -> rule8) triple16) -> rule5))] @2: Bob is kind.[(((((triple4 triple2) -> rule8) triple4) -> rule5))] Erin is kind.[(((((triple12 triple10) -> rule8) triple12) -> rule5))] @3: Bob is rough.[(((((((triple4 triple2) -> rule8) triple4) -> rule5) triple3) -> rule4))] Erin is rough.[(((((((triple12 triple10) -> rule8) triple12) -> rule5) triple11) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple4 triple2) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple8) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple9
((((triple12 triple10) -> (rule8 % int2)) triple10) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple16 triple14) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple16 ((triple15) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple14
((triple15) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Bob is cold.
("Bob" "is" "cold" "+")
((triple4 triple2) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple12 triple10) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple13 triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple16 triple14) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16 triple14) -> (rule8 % int3)) ((triple15) -> (rule2 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) ((triple15) -> (rule2 % int3))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((triple13 triple16) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple16 triple14) -> (rule8 % int2)) triple16) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule8 % int2)) triple16) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple4 triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple12 triple10) -> (rule8 % int2)) triple12) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple4 triple2) -> (rule8 % int3)) triple4) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple12 triple10) -> (rule8 % int3)) triple12) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3