Dave is not red. Fiona is red. Gary is blue. Harry is nice. All nice things are kind. If something is nice and not blue then it is kind. If something is rough and not green then it is not red. If something is big and not rough then it is red. If something is big then it is red. All red things are big. Blue things are big. If something is blue and big then it is nice.
Dave is not red.
("Dave" "is" "red" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is nice and not blue then it is kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
If something is rough and not green then it is not red.
((("something" "is" "rough" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "-"))
If something is big and not rough then it is red.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is blue and big then it is nice.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Gary is blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Gary is big.
True
2
proof
[(((triple3) -> rule7))]
("Gary" "is" "big" "+")
((triple3) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is red.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("Gary" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((triple3 ((triple3) -> rule7)) -> rule8))]
("Gary" "is" "nice" "-")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
True
5
proof
[(((((triple3 ((triple3) -> rule7)) -> rule8)) -> rule1))]
("Gary" "is" "kind" "+")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not kind.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule7)) -> rule8)) -> rule1))]
("Gary" "is" "kind" "-")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Dave" "is" "kind" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is not red.[(triple1)] Fiona is red.[(triple2)] Gary is blue.[(triple3)] Harry is nice.[(triple4)] @1: Fiona is big.[(((triple2) -> rule6))] Gary is big.[(((triple3) -> rule7))] Harry is kind.[(((triple4) -> rule1))] @2: Gary is nice.[(((triple3 ((triple3) -> rule7)) -> rule8))] Gary is red.[(((((triple3) -> rule7)) -> rule5))] @3: Gary is kind.[(((((triple3 ((triple3) -> rule7)) -> rule8)) -> rule1))]
Dave is not red.
("Dave" "is" "red" "-")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3