Fiona is red. Gary is round. Harry is rough. If something is rough then it is big. If something is green and kind then it is red. If Gary is red then Gary is green. Green things are red. If Gary is smart then Gary is rough. Big, rough things are green.
Fiona is red.
("Fiona" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is green and kind then it is red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Gary is red then Gary is green.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "green" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Gary is smart then Gary is rough.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "rough" "+"))
Big, rough things are green.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Fiona is red.
True
1
proof
[(triple1)]
("Fiona" "is" "red" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "red" "-")
triple1
Harry is big.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "-")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule6))]
("Harry" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule6))]
("Harry" "is" "green" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
True
5
proof
[(((((((triple3) -> rule1) triple3) -> rule6)) -> rule4))]
("Harry" "is" "red" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((((triple3) -> rule1) triple3) -> rule6)) -> rule4))]
("Harry" "is" "red" "-")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Fiona is red.[(triple1)] Gary is round.[(triple2)] Harry is rough.[(triple3)] @1: Harry is big.[(((triple3) -> rule1))] @2: Harry is green.[(((((triple3) -> rule1) triple3) -> rule6))] @3: Harry is red.[(((((((triple3) -> rule1) triple3) -> rule6)) -> rule4))]
Fiona is red.
("Fiona" "is" "red" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3