Bob is not green. Fiona is not green. Fiona is nice. Fiona is young. Gary is red. Harry is big. Harry is young. Cold people are green. Green, big people are round. If someone is young and big then they are cold. If Bob is green then Bob is big. If someone is young and not green then they are not red. If someone is round then they are red. If Harry is red and Harry is green then Harry is not nice.
Bob is not green.
("Bob" "is" "green" "-")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Green, big people are round.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is young and big then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Bob is green then Bob is big.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "big" "+"))
If someone is young and not green then they are not red.
((("someone" "is" "young" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "-"))
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Harry is red and Harry is green then Harry is not nice.
((("Harry" "is" "red" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "-"))
Fiona is young.
True
1
proof
[(triple4)]
("Fiona" "is" "young" "+")
triple4
Fiona is green.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "green" "+")
triple2
Harry is cold.
True
3
proof
[(((triple7 triple6) -> rule3))]
("Harry" "is" "cold" "+")
((triple7 triple6) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Fiona is red.
False
3
inv-proof
[(((triple4 triple2) -> rule5))]
("Fiona" "is" "red" "+")
((triple4 triple2) -> (rule5 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Harry is green.
True
4
proof
[(((((triple7 triple6) -> rule3)) -> rule1))]
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple7 triple6) -> rule3)) -> rule1))]
("Harry" "is" "green" "-")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
True
6
proof
[(((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2))]
("Harry" "is" "round" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not round.
False
6
inv-proof
[(((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2))]
("Harry" "is" "round" "-")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
True
7
proof
[(((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6))]
("Harry" "is" "red" "+")
((((((((triple7 triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not red.
False
7
inv-proof
[(((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6))]
("Harry" "is" "red" "-")
((((((((triple7 triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not nice.
True
12
proof
[(((((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6) ((((triple7 triple6) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "nice" "-")
((((((((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2)) ((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is nice.
False
12
inv-proof
[(((((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6) ((((triple7 triple6) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "nice" "+")
((((((((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2)) ((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is not green.[(triple1)] Fiona is nice.[(triple3)] Fiona is not green.[(triple2)] Fiona is young.[(triple4)] Gary is red.[(triple5)] Harry is big.[(triple6)] Harry is young.[(triple7)] @1: Fiona is not red.[(((triple4 triple2) -> rule5))] Harry is cold.[(((triple7 triple6) -> rule3))] @2: Harry is green.[(((((triple7 triple6) -> rule3)) -> rule1))] @3: Harry is round.[(((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2))] @4: Harry is red.[(((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6))] @5: Harry is not nice.[(((((((((((triple7 triple6) -> rule3)) -> rule1) triple6) -> rule2)) -> rule6) ((((triple7 triple6) -> rule3)) -> rule1)) -> rule7))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is not green.
("Fiona" "is" "green" "-")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Fiona is not red.
("Fiona" "is" "red" "-")
((triple4 triple2) -> (rule5 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 triple6) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple7 triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not nice.
("Harry" "is" "nice" "-")
((((((((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2)) ((((triple7 triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule7 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5