Anne is white. Bob is rough. Dave is red. Harry is young. All blue people are young. All red, blue people are big. If someone is young and big then they are rough. If someone is young then they are big. If Anne is red then Anne is white. If someone is red then they are big. Red people are rough. Big people are quiet.
Anne is white.
("Anne" "is" "white" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All red, blue people are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is young and big then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If Anne is red then Anne is white.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "white" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Harry is young.
True
1
proof
[(triple4)]
("Harry" "is" "young" "+")
triple4
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Dave is big.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "big" "+")
((triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "big" "-")
((triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple4) -> rule4)) -> rule8))]
("Harry" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((triple4 ((triple4) -> rule4)) -> rule3))]
("Harry" "is" "rough" "-")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is quiet.
Unknown
rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is white.[(triple1)] Bob is rough.[(triple2)] Dave is red.[(triple3)] Harry is young.[(triple4)] @1: Dave is big.[(((triple3) -> rule6))] Dave is rough.[(((triple3) -> rule7))] Harry is big.[(((triple4) -> rule4))] @2: Dave is quiet.[(((((triple3) -> rule6)) -> rule8))] Harry is quiet.[(((((triple4) -> rule4)) -> rule8))] Harry is rough.[(((triple4 ((triple4) -> rule4)) -> rule3))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2