Anne is smart. Anne is white. Bob is rough. Bob is smart. Fiona is big. Gary is kind. Gary is rough. If Bob is blue then Bob is big. If something is big and kind then it is green. All smart things are white. Green, white things are rough. If something is big then it is rough. If something is green then it is smart. If something is smart and not big then it is kind. All rough, smart things are kind. All rough things are kind.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Bob is blue then Bob is big.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "big" "+"))
If something is big and kind then it is green.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Green, white things are rough.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not big then it is kind.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
All rough, smart things are kind.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Gary is rough.
True
1
proof
[(triple7)]
("Gary" "is" "rough" "+")
triple7
Bob is not smart.
False
1
inv-proof
[(triple4)]
("Bob" "is" "smart" "-")
triple4
Fiona is rough.
True
2
proof
[(((triple5) -> rule5))]
("Fiona" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple5) -> rule5))]
("Fiona" "is" "rough" "-")
((triple5) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
True
3
proof
[(((((triple5) -> rule5)) -> rule9))]
("Fiona" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule9 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule9))]
("Fiona" "is" "kind" "-")
((((triple5) -> (rule5 % int2))) -> (rule9 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
True
5
proof
[(((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2))]
("Fiona" "is" "green" "+")
((triple5 ((((triple5) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not green.
False
5
inv-proof
[(((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2))]
("Fiona" "is" "green" "-")
((triple5 ((((triple5) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is smart.
True
6
proof
[(((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "+")
((((triple5 ((((triple5) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is not smart.
False
6
inv-proof
[(((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "-")
((((triple5 ((((triple5) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is white.
True
7
proof
[(((((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6)) -> rule3))]
("Fiona" "is" "white" "+")
((((((triple5 ((((triple5) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Fiona is not white.
False
7
inv-proof
[(((((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6)) -> rule3))]
("Fiona" "is" "white" "-")
((((((triple5 ((((triple5) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@3: Anne is kind.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule2 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is smart.[(triple1)] Anne is white.[(triple2 OR ((triple1) -> rule3))] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Fiona is big.[(triple5)] Gary is kind.[(triple6 OR ((triple7) -> rule9))] Gary is rough.[(triple7)] @1: Bob is kind.[(((triple3) -> rule9) OR ((triple3 triple4) -> rule8))] Bob is white.[(((triple4) -> rule3))] Fiona is rough.[(((triple5) -> rule5))] @2: Fiona is kind.[(((((triple5) -> rule5)) -> rule9))] @3: Fiona is green.[(((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2))] @4: Fiona is smart.[(((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6))] @5: Fiona is white.[(((((((triple5 ((((triple5) -> rule5)) -> rule9)) -> rule2)) -> rule6)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
((triple7) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 triple4) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple5) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule9 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple5 ((((triple5) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple5 ((((triple5) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple5 ((((triple5) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5