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