Anne is big. Dave is big. Gary is rough. Harry is rough. All green people are nice. Big people are green. All nice people are round.
Anne is big.
("Anne" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple4)]
("Harry" "is" "rough" "-")
triple4
Anne is green.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "-")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is round.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "round" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Harry" "is" "round" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is big.[(triple1)] Dave is big.[(triple2)] Gary is rough.[(triple3)] Harry is rough.[(triple4)] @1: Anne is green.[(((triple1) -> rule2))] Dave is green.[(((triple2) -> rule2))] @2: Anne is nice.[(((((triple1) -> rule2)) -> rule1))] Dave is nice.[(((((triple2) -> rule2)) -> rule1))] @3: Anne is round.[(((((((triple1) -> rule2)) -> rule1)) -> rule3))] Dave is round.[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3