Bob is cold. Bob is young. Charlie is cold. Fiona is furry. Harry is cold. Harry is green. Harry is rough. Blue, furry things are not green. All furry things are green. All cold things are red. If Charlie is not green then Charlie is young. All red, furry things are not young. If something is green then it is rough. Cold, young things are not rough. All blue, red things are cold. All rough, green things are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Blue, furry things are not green.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
All furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Charlie is not green then Charlie is young.
((("Charlie" "is" "green" "~")) -> ("Charlie" "is" "young" "+"))
All red, furry things are not young.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "-"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Cold, young things are not rough.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
All blue, red things are cold.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All rough, green things are cold.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule6))]
("Harry" "is" "rough" "-")
triple7
((triple6) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is red.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "red" "+")
((triple3) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is rough.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("Bob" "is" "rough" "+")
((triple1 triple2) -> (rule7 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Fiona is rough.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "rough" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "rough" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
True
6
proof
[(((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9))]
("Fiona" "is" "cold" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) ((triple4) -> (rule2 % int3))) -> (rule9 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not cold.
False
6
inv-proof
[(((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9))]
("Fiona" "is" "cold" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) ((triple4) -> (rule2 % int3))) -> (rule9 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is red.
True
7
proof
[(((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3))]
("Fiona" "is" "red" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is not red.
False
7
inv-proof
[(((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3))]
("Fiona" "is" "red" "-")
((((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is not young.
True
9
proof
[(((((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3) triple4) -> rule5))]
("Fiona" "is" "young" "-")
((((((((((triple4) -> (rule2 % int5))) -> (rule6 % int4)) ((triple4) -> (rule2 % int5))) -> (rule9 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Fiona is young.
False
9
inv-proof
[(((((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3) triple4) -> rule5))]
("Fiona" "is" "young" "+")
((((((((((triple4) -> (rule2 % int5))) -> (rule6 % int4)) ((triple4) -> (rule2 % int5))) -> (rule9 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is young.[(triple2)] Charlie is cold.[(triple3)] Fiona is furry.[(triple4)] Harry is cold.[(triple5 OR ((triple7 triple6) -> rule9) OR ((((triple6) -> rule6) triple6) -> rule9))] Harry is green.[(triple6)] Harry is rough.[(triple7 OR ((triple6) -> rule6))] @1: Bob is not rough.[(((triple1 triple2) -> rule7))] Bob is red.[(((triple1) -> rule3))] Charlie is red.[(((triple3) -> rule3))] Fiona is green.[(((triple4) -> rule2))] Harry is red.[(((triple5) -> rule3) OR ((((triple7 triple6) -> rule9)) -> rule3) OR ((((((triple6) -> rule6) triple6) -> rule9)) -> rule3))] @2: Fiona is rough.[(((((triple4) -> rule2)) -> rule6))] @3: Fiona is cold.[(((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9))] @4: Fiona is red.[(((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3))] @5: Fiona is not young.[(((((((((((triple4) -> rule2)) -> rule6) ((triple4) -> rule2)) -> rule9)) -> rule3) triple4) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
((triple7 triple6) -> (rule9 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2)) triple6) -> (rule9 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
((triple1 triple2) -> (rule7 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple4) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple5) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple7 triple6) -> (rule9 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple6) -> (rule6 % int3)) triple6) -> (rule9 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) ((triple4) -> (rule2 % int3))) -> (rule9 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is not young.
("Fiona" "is" "young" "-")
((((((((((triple4) -> (rule2 % int5))) -> (rule6 % int4)) ((triple4) -> (rule2 % int5))) -> (rule9 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5