Anne is nice. Erin is nice. Fiona is round. Harry is green. Green people are big. If someone is big then they are blue. If Harry is blue then Harry is rough. Blue people are big. Rough people are green. If Anne is rough then Anne is round.
Anne is nice.
("Anne" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Harry is blue then Harry is rough.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "rough" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Anne is rough then Anne is round.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "round" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple2)]
("Erin" "is" "nice" "-")
triple2
Harry is big.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "big" "+")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "big" "-")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "blue" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "rough" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not rough.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "rough" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Erin is big.
Unknown
rconc
[@4: Erin is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- rule5 <- FAIL)]]
("Erin" "is" "big" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is blue.
Unknown
rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "blue" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is nice.[(triple1)] Erin is nice.[(triple2)] Fiona is round.[(triple3)] Harry is green.[(triple4)] @1: Harry is big.[(((triple4) -> rule1))] @2: Harry is blue.[(((((triple4) -> rule1)) -> rule2))] @3: Harry is rough.[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3