Charlie is blue. Charlie is cold. Charlie is red. Charlie is rough. Dave is cold. Dave is kind. Dave is red. Dave is rough. Dave is round. Fiona is nice. Fiona is red. Harry is blue. Harry is cold. Harry is nice. Harry is round. If something is rough and round then it is red. All red things are round. If something is blue then it is rough. If Dave is rough and Dave is nice then Dave is red. If Harry is round then Harry is rough. If something is rough and blue then it is cold. Round, rough things are kind. Blue things are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is rough and round then it is red.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Dave is rough and Dave is nice then Dave is red.
((("Dave" "is" "rough" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "red" "+"))
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
If something is rough and blue then it is cold.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Round, rough things are kind.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Dave is not kind.
False
1
inv-proof
[(triple6 OR ((triple9 triple8) -> rule7) OR ((((triple7) -> rule2) triple8) -> rule7))]
("Dave" "is" "kind" "-")
triple6
((triple9 triple8) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple7) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is round.
True
2
proof
[(((triple11) -> rule2))]
("Fiona" "is" "round" "+")
((triple11) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple15) -> rule5))]
("Harry" "is" "rough" "-")
((triple12) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple15) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
True
4
proof
[(((((triple12) -> rule3) triple15) -> rule1) OR ((((triple15) -> rule5) triple15) -> rule1))]
("Harry" "is" "red" "+")
((((triple12) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15) -> (rule5 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not red.
False
4
inv-proof
[(((((triple12) -> rule3) triple15) -> rule1) OR ((((triple15) -> rule5) triple15) -> rule1))]
("Harry" "is" "red" "-")
((((triple12) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15) -> (rule5 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((triple4 triple1) -> rule6) OR ((((triple1) -> rule3) triple1) -> rule6))] Charlie is red.[(triple3)] Charlie is rough.[(triple4 OR ((triple1) -> rule3))] Dave is cold.[(triple5)] Dave is kind.[(triple6 OR ((triple9 triple8) -> rule7) OR ((((triple7) -> rule2) triple8) -> rule7))] Dave is red.[(triple7 OR ((triple8 triple9) -> rule1))] Dave is rough.[(triple8)] Dave is round.[(triple9 OR ((triple7) -> rule2))] Fiona is nice.[(triple10)] Fiona is red.[(triple11)] Harry is blue.[(triple12)] Harry is cold.[(triple13 OR ((((triple12) -> rule3) triple12) -> rule6) OR ((((triple15) -> rule5) triple12) -> rule6))] Harry is nice.[(triple14)] Harry is round.[(triple15)] @1: Charlie is kind.[(((triple1) -> rule8) OR ((((triple3) -> rule2) triple4) -> rule7) OR ((((triple3) -> rule2) ((triple1) -> rule3)) -> rule7))] Charlie is round.[(((triple3) -> rule2))] Fiona is round.[(((triple11) -> rule2))] Harry is kind.[(((triple12) -> rule8) OR ((triple15 ((triple12) -> rule3)) -> rule7) OR ((triple15 ((triple15) -> rule5)) -> rule7))] Harry is rough.[(((triple12) -> rule3) OR ((triple15) -> rule5))] @2: Harry is red.[(((((triple12) -> rule3) triple15) -> rule1) OR ((((triple15) -> rule5) triple15) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
((triple9 triple8) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple7) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple8 triple9) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((((triple12) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple3) -> (rule2 % int2)) triple4) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple11) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple12) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple15 ((triple12) -> (rule3 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple15 ((triple15) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple15) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple12) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple15) -> (rule5 % int2)) triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2