Bob is cold. Bob is green. Bob is kind. Bob is white. Charlie is blue. Charlie is cold. Charlie is green. Charlie is white. Erin is blue. Erin is cold. Erin is green. Erin is kind. Erin is round. Erin is smart. Erin is white. Harry is green. If Harry is cold and Harry is blue then Harry is green. All round people are kind. If Erin is blue and Erin is smart then Erin is round. If someone is cold then they are white. If someone is blue then they are smart. If Bob is cold and Bob is white then Bob is blue.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
If Harry is cold and Harry is blue then Harry is green.
((("Harry" "is" "cold" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Erin is blue and Erin is smart then Erin is round.
((("Erin" "is" "blue" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Bob is cold and Bob is white then Bob is blue.
((("Bob" "is" "cold" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "+"))
Charlie is green.
True
1
proof
[(triple7)]
("Charlie" "is" "green" "+")
triple7
Erin is not round.
False
1
inv-proof
[(triple13 OR ((triple9 triple14) -> rule3) OR ((triple9 ((triple9) -> rule5)) -> rule3))]
("Erin" "is" "round" "-")
triple13
((triple9 triple14) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple9 ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Charlie is smart.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple5) -> rule5))]
("Charlie" "is" "smart" "-")
((triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is smart.
True
4
proof
[(((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule5))]
("Bob" "is" "smart" "+")
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule5))]
("Bob" "is" "smart" "-")
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is white.[(triple4 OR ((triple1) -> rule4))] Charlie is blue.[(triple5)] Charlie is cold.[(triple6)] Charlie is green.[(triple7)] Charlie is white.[(triple8 OR ((triple6) -> rule4))] Erin is blue.[(triple9)] Erin is cold.[(triple10)] Erin is green.[(triple11)] Erin is kind.[(triple12 OR ((triple13) -> rule2) OR ((((triple9 triple14) -> rule3)) -> rule2) OR ((((triple9 ((triple9) -> rule5)) -> rule3)) -> rule2))] Erin is round.[(triple13 OR ((triple9 triple14) -> rule3) OR ((triple9 ((triple9) -> rule5)) -> rule3))] Erin is smart.[(triple14 OR ((triple9) -> rule5))] Erin is white.[(triple15 OR ((triple10) -> rule4))] Harry is green.[(triple16)] @1: Bob is blue.[(((triple1 triple4) -> rule6) OR ((triple1 ((triple1) -> rule4)) -> rule6))] Charlie is smart.[(((triple5) -> rule5))] @2: Bob is smart.[(((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is cold.
("Erin" "is" "cold" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
triple11
Erin is kind.
("Erin" "is" "kind" "+")
triple12
((triple13) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple9 triple14) -> (rule3 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple9 ((triple9) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple13
((triple9 triple14) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple9 ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple14
((triple9) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple15
((triple10) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple16
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3