Bob is rough. Bob is smart. Charlie is quiet. Charlie is young. Fiona is quiet. Gary is blue. Gary is furry. Gary is quiet. Gary is smart. Gary is young. If Charlie is quiet and Charlie is kind then Charlie is smart. If someone is furry then they are young. Young people are kind. All rough people are kind. If Bob is quiet then Bob is blue. If someone is kind and rough then they are furry. Young people are quiet.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Charlie is quiet and Charlie is kind then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "smart" "+"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If Bob is quiet then Bob is blue.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "blue" "+"))
If someone is kind and rough then they are furry.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "-")
triple1
Bob is kind.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple10) -> rule3) OR ((((triple7) -> rule2)) -> rule3))]
("Gary" "is" "kind" "-")
((triple10) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is smart.
True
4
proof
[(((triple3 ((triple4) -> rule3)) -> rule1) OR ((((triple4) -> rule7) ((triple4) -> rule3)) -> rule1))]
("Charlie" "is" "smart" "+")
((triple3 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
True
5
proof
[(((((((triple1) -> rule4) triple1) -> rule6)) -> rule2))]
("Bob" "is" "young" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not young.
False
5
inv-proof
[(((((((triple1) -> rule4) triple1) -> rule6)) -> rule2))]
("Bob" "is" "young" "-")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
True
6
proof
[(((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7))]
("Bob" "is" "quiet" "+")
((((((((triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not quiet.
False
6
inv-proof
[(((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7))]
("Bob" "is" "quiet" "-")
((((((((triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is blue.
True
7
proof
[(((((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7)) -> rule5))]
("Bob" "is" "blue" "+")
((((((((((triple1) -> (rule4 % int5)) triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is not blue.
False
7
inv-proof
[(((((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7)) -> rule5))]
("Bob" "is" "blue" "-")
((((((((((triple1) -> (rule4 % int5)) triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is rough.[(triple1)] Bob is smart.[(triple2)] Charlie is quiet.[(triple3 OR ((triple4) -> rule7))] Charlie is young.[(triple4)] Fiona is quiet.[(triple5)] Gary is blue.[(triple6)] Gary is furry.[(triple7)] Gary is quiet.[(triple8 OR ((triple10) -> rule7) OR ((((triple7) -> rule2)) -> rule7))] Gary is smart.[(triple9)] Gary is young.[(triple10 OR ((triple7) -> rule2))] @1: Bob is kind.[(((triple1) -> rule4))] Charlie is kind.[(((triple4) -> rule3))] Gary is kind.[(((triple10) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] @2: Bob is furry.[(((((triple1) -> rule4) triple1) -> rule6))] Charlie is smart.[(((triple3 ((triple4) -> rule3)) -> rule1) OR ((((triple4) -> rule7) ((triple4) -> rule3)) -> rule1))] @3: Bob is young.[(((((((triple1) -> rule4) triple1) -> rule6)) -> rule2))] @4: Bob is quiet.[(((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7))] @5: Bob is blue.[(((((((((((triple1) -> rule4) triple1) -> rule6)) -> rule2)) -> rule7)) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple4) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((triple10) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((((triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
((((((((((triple1) -> (rule4 % int5)) triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5