Dave is big. Dave is cold. Dave is kind. Dave is white. Fiona is big. Fiona is green. Fiona is kind. Harry is cold. Harry is rough. Harry is white. All kind, rough things are green. Big things are round. Cold things are kind. If something is big then it is round. If Fiona is rough and Fiona is white then Fiona is green. If something is round and cold then it is white. If something is rough then it is big. If Harry is big then Harry is cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind, rough things are green.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Fiona is rough and Fiona is white then Fiona is green.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "green" "+"))
If something is round and cold then it is white.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Harry is big then Harry is cold.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "cold" "+"))
Dave is kind.
True
1
proof
[(triple3 OR ((triple2) -> rule3))]
("Dave" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is not rough.
False
1
inv-proof
[(triple9)]
("Harry" "is" "rough" "-")
triple9
Dave is round.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule4))]
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple8) -> rule3) OR ((((((triple9) -> rule7)) -> rule8)) -> rule3))]
("Harry" "is" "kind" "-")
((triple8) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((((triple9) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is green.
True
4
proof
[(((((triple8) -> rule3) triple9) -> rule1) OR ((((((((triple9) -> rule7)) -> rule8)) -> rule3) triple9) -> rule1))]
("Harry" "is" "green" "+")
((((triple8) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((((triple9) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not green.
False
4
inv-proof
[(((((triple8) -> rule3) triple9) -> rule1) OR ((((((((triple9) -> rule7)) -> rule8)) -> rule3) triple9) -> rule1))]
("Harry" "is" "green" "-")
((((triple8) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((((triple9) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3 OR ((triple2) -> rule3))] Dave is white.[(triple4 OR ((((triple1) -> rule2) triple2) -> rule6) OR ((((triple1) -> rule4) triple2) -> rule6))] Fiona is big.[(triple5)] Fiona is green.[(triple6)] Fiona is kind.[(triple7)] Harry is cold.[(triple8 OR ((((triple9) -> rule7)) -> rule8))] Harry is rough.[(triple9)] Harry is white.[(triple10 OR ((((((triple9) -> rule7)) -> rule2) triple8) -> rule6) OR ((((((triple9) -> rule7)) -> rule4) triple8) -> rule6) OR ((((((triple9) -> rule7)) -> rule2) ((((triple9) -> rule7)) -> rule8)) -> rule6) OR ((((((triple9) -> rule7)) -> rule4) ((((triple9) -> rule7)) -> rule8)) -> rule6))] @1: Dave is round.[(((triple1) -> rule2) OR ((triple1) -> rule4))] Fiona is round.[(((triple5) -> rule2) OR ((triple5) -> rule4))] Harry is big.[(((triple9) -> rule7))] Harry is kind.[(((triple8) -> rule3) OR ((((((triple9) -> rule7)) -> rule8)) -> rule3))] @2: Harry is green.[(((((triple8) -> rule3) triple9) -> rule1) OR ((((((((triple9) -> rule7)) -> rule8)) -> rule3) triple9) -> rule1))] Harry is round.[(((((triple9) -> rule7)) -> rule2) OR ((((triple9) -> rule7)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple4
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple1) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((((triple9) -> (rule7 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((((((triple9) -> (rule7 % int3))) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple9) -> (rule7 % int4))) -> (rule2 % int3)) ((((triple9) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((((triple9) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple9) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple5) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple5) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple9) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((((triple9) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((triple8) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((((triple9) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2