Charlie is cold. Charlie is round. Dave is cold. Dave is furry. Dave is nice. Dave is red. Dave is round. Dave is smart. Fiona is nice. Fiona is round. If something is nice and smart then it is cold. All round, young things are smart. If something is nice then it is smart. All smart, round things are cold. If something is furry and nice then it is red. If Dave is cold then Dave is smart.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If something is nice and smart then it is cold.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All round, young things are smart.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All smart, round things are cold.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is furry and nice then it is red.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Dave is cold then Dave is smart.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "smart" "+"))
Dave is nice.
True
1
proof
[(triple5)]
("Dave" "is" "nice" "+")
triple5
Dave is not cold.
False
1
inv-proof
[(triple3 OR ((triple5 triple8) -> rule1) OR ((triple8 triple7) -> rule4) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule3) triple7) -> rule4))]
("Dave" "is" "cold" "-")
triple3
((triple5 triple8) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple8 triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple5) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Charlie is cold.[(triple1)] Charlie is round.[(triple2)] Dave is cold.[(triple3 OR ((triple5 triple8) -> rule1) OR ((triple8 triple7) -> rule4) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule3) triple7) -> rule4))] Dave is furry.[(triple4)] Dave is nice.[(triple5)] Dave is red.[(triple6 OR ((triple4 triple5) -> rule5))] Dave is round.[(triple7)] Dave is smart.[(triple8 OR ((triple3) -> rule6) OR ((triple5) -> rule3))] Fiona is nice.[(triple9)] Fiona is round.[(triple10)] @1: Fiona is smart.[(((triple9) -> rule3))] @2: Fiona is cold.[(((triple9 ((triple9) -> rule3)) -> rule1) OR ((((triple9) -> rule3) triple10) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple5 triple8) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple8 triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple5) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple4 triple5) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((triple3) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple9) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2