Bob is big. Bob is kind. Bob is rough. Charlie is round. Charlie is young. Dave is blue. Dave is kind. Dave is rough. Dave is smart. Fiona is young. If something is big then it is rough. All round, young things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All round, young things are big.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Charlie is not young.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "young" "-")
triple5
Charlie is big.
True
3
proof
[(((triple4 triple5) -> rule2))]
("Charlie" "is" "big" "+")
((triple4 triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
3
inv-proof
[(((triple4 triple5) -> rule2))]
("Charlie" "is" "big" "-")
((triple4 triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
True
4
proof
[(((((triple4 triple5) -> rule2)) -> rule1))]
("Charlie" "is" "rough" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((((triple4 triple5) -> rule2)) -> rule1))]
("Charlie" "is" "rough" "-")
((((triple4 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is rough.[(triple3 OR ((triple1) -> rule1))] Charlie is round.[(triple4)] Charlie is young.[(triple5)] Dave is blue.[(triple6)] Dave is kind.[(triple7)] Dave is rough.[(triple8)] Dave is smart.[(triple9)] Fiona is young.[(triple10)] @1: Charlie is big.[(((triple4 triple5) -> rule2))] @2: Charlie is rough.[(((((triple4 triple5) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Charlie is big.
("Charlie" "is" "big" "+")
((triple4 triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2