Bob is cold. Bob is quiet. Bob is round. Charlie is quiet. Erin is quiet. Erin is young. Harry is not young. Rough people are cold. All young, quiet people are cold. Quiet, blue people are round. Green people are rough. If someone is quiet then they are rough. Cold, rough people are not green.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is not young.
("Harry" "is" "young" "-")
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All young, quiet people are cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Quiet, blue people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Cold, rough people are not green.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
Erin is quiet.
True
1
proof
[(triple5)]
("Erin" "is" "quiet" "+")
triple5
Harry is young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Erin is cold.
True
3
proof
[(((triple6 triple5) -> rule2) OR ((((triple5) -> rule5)) -> rule1))]
("Erin" "is" "cold" "+")
((triple6 triple5) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Charlie is not rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("Charlie" "is" "rough" "-")
((triple4) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Bob is not green.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule6) OR ((((((triple2) -> rule5)) -> rule1) ((triple2) -> rule5)) -> rule6))]
("Bob" "is" "green" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is not cold.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule1))]
("Charlie" "is" "cold" "-")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not green.
True
6
proof
[(((((((triple4) -> rule5)) -> rule1) ((triple4) -> rule5)) -> rule6))]
("Charlie" "is" "green" "-")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is green.
False
6
inv-proof
[(((((((triple4) -> rule5)) -> rule1) ((triple4) -> rule5)) -> rule6))]
("Charlie" "is" "green" "+")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Harry" "is" "cold" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is cold.[(triple1 OR ((((triple2) -> rule5)) -> rule1))] Bob is quiet.[(triple2)] Bob is round.[(triple3)] Charlie is quiet.[(triple4)] Erin is quiet.[(triple5)] Erin is young.[(triple6)] Harry is not young.[(triple7)] @1: Bob is rough.[(((triple2) -> rule5))] Charlie is rough.[(((triple4) -> rule5))] Erin is cold.[(((triple6 triple5) -> rule2) OR ((((triple5) -> rule5)) -> rule1))] Erin is rough.[(((triple5) -> rule5))] @2: Bob is not green.[(((triple1 ((triple2) -> rule5)) -> rule6) OR ((((((triple2) -> rule5)) -> rule1) ((triple2) -> rule5)) -> rule6))] Charlie is cold.[(((((triple4) -> rule5)) -> rule1))] Erin is not green.[(((((triple6 triple5) -> rule2) ((triple5) -> rule5)) -> rule6) OR ((((((triple5) -> rule5)) -> rule1) ((triple5) -> rule5)) -> rule6))] @3: Charlie is not green.[(((((((triple4) -> rule5)) -> rule1) ((triple4) -> rule5)) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is not young.
("Harry" "is" "young" "-")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple6 triple5) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((((triple6 triple5) -> (rule2 % int3)) ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2)) ((triple5) -> (rule5 % int3))) -> (rule6 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Charlie is not green.
("Charlie" "is" "green" "-")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) ((triple4) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3