Dave is nice. Harry is blue. Harry is young. If something is rough and nice then it is cold. Big things are rough. If something is big and young then it is green. Nice things are not green. If something is nice then it is big. If something is nice and not young then it is not big. Cold things are big. If Harry is blue then Harry is not big.
Dave is nice.
("Dave" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is rough and nice then it is cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is big and young then it is green.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Nice things are not green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is nice and not young then it is not big.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "-"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Harry is blue then Harry is not big.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "big" "-"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Dave is big.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "big" "+")
((triple1) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "big" "-")
((triple1) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
True
5
proof
[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Dave is nice.[(triple1)] Harry is blue.[(triple2)] Harry is young.[(triple3)] @1: Dave is big.[(((triple1) -> rule5))] Dave is not green.[(((triple1) -> rule4))] Harry is not big.[(((triple2) -> rule8))] @2: Dave is rough.[(((((triple1) -> rule5)) -> rule2))] @3: Dave is cold.[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple1) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is not big.
("Harry" "is" "big" "-")
((triple2) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3