Anne is green. Charlie is blue. Charlie is cold. Charlie is green. Charlie is red. Dave is round. Fiona is not blue. Fiona is cold. Fiona is green. Fiona is red. Fiona is round. Fiona is smart. If someone is green then they are cold. If Dave is not blue then Dave is not round. Furry, smart people are red. If someone is cold and blue then they are round. If someone is blue and cold then they are green. Smart people are green. Blue people are smart. If Dave is not smart then Dave is red.
Anne is green.
("Anne" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Dave is not blue then Dave is not round.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "round" "-"))
Furry, smart people are red.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and blue then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and cold then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Dave is not smart then Dave is red.
((("Dave" "is" "smart" "~")) -> ("Dave" "is" "red" "+"))
Charlie is cold.
True
1
proof
[(triple3 OR ((triple4) -> rule1) OR ((((((triple2) -> rule7)) -> rule6)) -> rule1))]
("Charlie" "is" "cold" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Fiona is not red.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "red" "-")
triple10
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule4) OR ((((triple4) -> rule1) triple2) -> rule4) OR ((((((((triple2) -> rule7)) -> rule6)) -> rule1) triple2) -> rule4))]
("Charlie" "is" "round" "-")
((triple3 triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Dave is not cold.
Unknown
inv-rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule7 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "smart" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is green.[(triple1)] Charlie is blue.[(triple2)] Charlie is cold.[(triple3 OR ((triple4) -> rule1) OR ((((((triple2) -> rule7)) -> rule6)) -> rule1))] Charlie is green.[(triple4 OR ((triple2 triple3) -> rule5) OR ((((triple2) -> rule7)) -> rule6))] Charlie is red.[(triple5)] Dave is round.[(triple6)] Fiona is cold.[(triple8 OR ((triple9) -> rule1) OR ((((triple12) -> rule6)) -> rule1))] Fiona is green.[(triple9 OR ((triple12) -> rule6))] Fiona is not blue.[(triple7)] Fiona is red.[(triple10)] Fiona is round.[(triple11)] Fiona is smart.[(triple12)] @1: Anne is cold.[(((triple1) -> rule1))] Charlie is round.[(((triple3 triple2) -> rule4) OR ((((triple4) -> rule1) triple2) -> rule4) OR ((((((((triple2) -> rule7)) -> rule6)) -> rule1) triple2) -> rule4))] Charlie is smart.[(((triple2) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple2 triple3) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple9) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple9
((triple12) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((((triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1