Bob is rough. Dave is green. Erin is kind. Harry is red. Nice people are round. Green, red people are big. If someone is red then they are rough. Big people are nice. If Bob is round then Bob is kind. If someone is green then they are red.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Green, red people are big.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If Bob is round then Bob is kind.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Harry is red.
True
1
proof
[(triple4)]
("Harry" "is" "red" "+")
triple4
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Dave is red.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "red" "+")
((triple2) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
True
5
proof
[(((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4))]
("Dave" "is" "nice" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4))]
("Dave" "is" "nice" "-")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule2 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "+")
Bob is not kind.
Unknown
inv-rconc
[@4: Bob is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is rough.[(triple1)] Dave is green.[(triple2)] Erin is kind.[(triple3)] Harry is red.[(triple4)] @1: Dave is red.[(((triple2) -> rule6))] Harry is rough.[(((triple4) -> rule3))] @2: Dave is big.[(((triple2 ((triple2) -> rule6)) -> rule2))] Dave is rough.[(((((triple2) -> rule6)) -> rule3))] @3: Dave is nice.[(((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4))] @4: Dave is round.[(((((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4