Bob is young. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. Erin is red. Erin is smart. Erin is young. Gary is cold. Gary is young. Cold people are white. All young people are green. All cold people are smart. If Charlie is green and Charlie is smart then Charlie is cold. If someone is green and young then they are white. If Gary is white and Gary is green then Gary is cold. All red, green people are white. If Gary is red and Gary is cold then Gary is smart.
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is green and Charlie is smart then Charlie is cold.
((("Charlie" "is" "green" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is green and young then they are white.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Gary is white and Gary is green then Gary is cold.
((("Gary" "is" "white" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "cold" "+"))
All red, green people are white.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Gary is red and Gary is cold then Gary is smart.
((("Gary" "is" "red" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
Charlie is white.
True
1
proof
[(triple4 OR ((((triple5) -> rule2) triple5) -> rule5) OR ((((((triple5) -> rule2) triple3) -> rule4)) -> rule1))]
("Charlie" "is" "white" "+")
triple4
((((triple5) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple5) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is young.[(triple1)] Charlie is round.[(triple2)] Charlie is smart.[(triple3)] Charlie is white.[(triple4 OR ((((triple5) -> rule2) triple5) -> rule5) OR ((((((triple5) -> rule2) triple3) -> rule4)) -> rule1))] Charlie is young.[(triple5)] Erin is red.[(triple6)] Erin is smart.[(triple7)] Erin is young.[(triple8)] Gary is cold.[(triple9 OR ((((((triple10) -> rule2) triple10) -> rule5) ((triple10) -> rule2)) -> rule6))] Gary is young.[(triple10)] @1: Bob is green.[(((triple1) -> rule2))] Charlie is green.[(((triple5) -> rule2))] Erin is green.[(((triple8) -> rule2))] Gary is green.[(((triple10) -> rule2))] Gary is smart.[(((triple9) -> rule3) OR ((((((((triple10) -> rule2) triple10) -> rule5) ((triple10) -> rule2)) -> rule6)) -> rule3))] Gary is white.[(((triple9) -> rule1) OR ((((triple10) -> rule2) triple10) -> rule5))] @2: Bob is white.[(((((triple1) -> rule2) triple1) -> rule5))] Charlie is cold.[(((((triple5) -> rule2) triple3) -> rule4))] Erin is white.[(((triple6 ((triple8) -> rule2)) -> rule7) OR ((((triple8) -> rule2) triple8) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((((triple5) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple5) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((((((triple10) -> (rule2 % int3)) triple10) -> (rule5 % int2)) ((triple10) -> (rule2 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple10
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple5) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple10) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((((((triple10) -> (rule2 % int4)) triple10) -> (rule5 % int3)) ((triple10) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple10) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple5) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple6 ((triple8) -> (rule2 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8) -> (rule2 % int2)) triple8) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2