Charlie is rough. Fiona is furry. Harry is big. If someone is green and red then they are cold. Furry, green people are red. If Fiona is furry then Fiona is green. All red people are green. If someone is cold then they are big. All big, rough people are green. If Charlie is cold then Charlie is rough. If someone is round and cold then they are rough.
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is green and red then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Furry, green people are red.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Fiona is furry then Fiona is green.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "green" "+"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All big, rough people are green.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Charlie is cold then Charlie is rough.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is round and cold then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Fiona is not furry.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "furry" "-")
triple2
Fiona is green.
True
2
proof
[(((triple2) -> rule3))]
("Fiona" "is" "green" "+")
((triple2) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Fiona" "is" "green" "-")
((triple2) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Fiona" "is" "red" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not red.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Fiona" "is" "red" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
True
7
proof
[(((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule1))]
("Fiona" "is" "cold" "+")
((((triple2) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not cold.
False
7
inv-proof
[(((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule1))]
("Fiona" "is" "cold" "-")
((((triple2) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "+")
Charlie is not green.
Unknown
inv-rconc
[@4: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "rough" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is rough.[(triple1)] Fiona is furry.[(triple2)] Harry is big.[(triple3)] @1: Fiona is green.[(((triple2) -> rule3))] @2: Fiona is red.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: Fiona is cold.[(((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule1))] @4: Fiona is big.[(((((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule1)) -> rule5))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
((triple2) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple2) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple2) -> (rule3 % int4)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4