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